#pragma once
#include "TermVariable.h"
#include "ArrowType.h"

using namespace std;


// ApplicationTerm command target

class ApplicationTerm : public Term
{

protected:
	TokenPair LeftRight;
	
protected:
    void ResolveType(Term::const_reference TL, Token::const_reference TR);

public:	 
	virtual Token::const_reference getRight() const;
	virtual Term::const_reference getLeft() const;

public:
	bool isApplicationTerm() const{return true;};
	virtual bool isRedex() const;

public:
	ApplicationTerm(Term::const_reference, Token::const_reference, const string& ="");
	ApplicationTerm(const ApplicationTerm&);
	virtual ~ApplicationTerm();

public:   	
	//Token Overides
	Token::pointer normalized() const;
	Token::pointer applyArgument(Token::const_reference)  const;
	Token::pointer clone() const;
	bool isReducible() const;
	string toString() const;
	string view() const;
	bool operator==(Token::const_reference To) const;
	Token::pointer replaceAll(Token::const_reference, Token::const_reference) const;
	COUNTER complexity() const {return getLeft().complexity()+getRight().complexity()+Term::complexity();};

public:
	bool TypeOccursinFreeVariable(Type::const_reference Ty) const;
};

class InvertedListTerm : public	Term{
		
public:
	bool isApplicationTerm() const{return true;};

protected:
	/************************
		((((0,1),2),3),4)
	************************/
	TokenVector  Applications;

public:	 
	Token::const_reference getRight() const;

public:
	InvertedListTerm(vector<Token*>, const string& ="");
	InvertedListTerm(Term::const_reference);
	InvertedListTerm(const InvertedListTerm&);
	virtual ~InvertedListTerm();

};

class VirtualInvertedListTerm : public	Term{
		
public:
	bool isApplicationTerm() const{return true;};

protected:
	/************************
		((((0,1),2),3),4)
	************************/
	vector<Token::pointer>  Applications;

public:	 
	Token::const_reference getRight() const;

public:
	VirtualInvertedListTerm(vector<Token*>, const string& ="");
//	VirtualInvertedListTerm(Term::const_reference);
//	VirtualInvertedListTerm(const VirtualInvertedListTerm&);
	virtual ~VirtualInvertedListTerm(){};

};






